L180493We prove the intermediate
claim HxX:
x ∈ X.
L180495An exact proof term for the current goal is (HAsubX x HxA).
L180495We prove the intermediate
claim H0:
State 0 = BaseState.
L180497An
exact proof term for the current goal is
(nat_primrec_0 BaseState StepState).
L180497rewrite the current goal using H0 (from left to right).
L180498We prove the intermediate
claim HBase:
BaseState = (g0g,(f1s,den)).
L180500rewrite the current goal using HBase (from left to right).
L180501rewrite the current goal using
(tuple_2_0_eq g0g (f1s,den)) (from left to right) at position 1.
L180502rewrite the current goal using
(tuple_2_1_eq g0g (f1s,den)) (from left to right) at position 1.
L180503rewrite the current goal using
(tuple_2_0_eq f1s den) (from left to right) at position 1.
L180504rewrite the current goal using
(tuple_2_1_eq g0g (f1s,den)) (from left to right) at position 1.
L180505rewrite the current goal using
(tuple_2_1_eq f1s den) (from left to right) at position 1.
L180509rewrite the current goal using Hg0g_app (from left to right) at position 1.
L180512An exact proof term for the current goal is (Hf1s_apply x HxA).
L180512rewrite the current goal using Hf1s_app (from left to right) at position 1.
L180513We prove the intermediate
claim Hf1xI2:
apply_fun f1 x ∈ I2.
L180515An exact proof term for the current goal is (Hf1_range x HxA).
L180518rewrite the current goal using HI2def (from left to right).
L180519An exact proof term for the current goal is Hf1xI2.
L180520We prove the intermediate
claim Hf1xR:
apply_fun f1 x ∈ R.
L180522We prove the intermediate
claim Hf1xS:
SNo (apply_fun f1 x).
L180526rewrite the current goal using HmulDiv (from left to right) at position 1.
L180527rewrite the current goal using (Hf1_apply x HxA) (from left to right) at position 1.
L180528We prove the intermediate
claim HfxR:
apply_fun f x ∈ R.
L180530An exact proof term for the current goal is (Hf_R x HxA).
L180532We prove the intermediate
claim Hg0I0:
apply_fun g0 x ∈ I0.
L180534An exact proof term for the current goal is (Hfung0 x HxX).
L180534We prove the intermediate
claim Hg0R:
apply_fun g0 x ∈ R.
L180544rewrite the current goal using
(add_SNo_0R (apply_fun f x) HfxS) (from left to right) at position 1.
Use reflexivity.
L180555We prove the intermediate
claim HS:
State (ordsucc k) = StepState k (State k).
L180557An
exact proof term for the current goal is
(nat_primrec_S BaseState StepState k HkNat).
L180557rewrite the current goal using HS (from left to right).
L180558rewrite the current goal using (IH x HxA) (from right to left).
L180559We prove the intermediate
claim HkO:
k ∈ ω.
L180561An
exact proof term for the current goal is
(nat_p_omega k HkNat).
L180561We prove the intermediate
claim HxX:
x ∈ X.
L180563An exact proof term for the current goal is (HAsubX x HxA).
L180563Set st to be the term State k.
L180564Set g to be the term
st 0.
L180565Set rpack to be the term
st 1.
L180566Set r to be the term
rpack 0.
L180567Set c to be the term
rpack 1.
L180576Set cNew to be the term
mul_SNo c den.
L180577We prove the intermediate
claim Hdef:
StepState k st = (gNew,(rNew,cNew)).
L180579We prove the intermediate
claim HgStep:
(StepState k st) 0 = gNew.
L180581rewrite the current goal using Hdef (from left to right).
L180581An
exact proof term for the current goal is
(tuple_2_0_eq gNew (rNew,cNew)).
L180582We prove the intermediate
claim HrpackStep:
(StepState k st) 1 = (rNew,cNew).
L180584rewrite the current goal using Hdef (from left to right).
L180584An
exact proof term for the current goal is
(tuple_2_1_eq gNew (rNew,cNew)).
L180585We prove the intermediate
claim HrStep:
((StepState k st) 1) 0 = rNew.
L180587rewrite the current goal using HrpackStep (from left to right).
L180587An
exact proof term for the current goal is
(tuple_2_0_eq rNew cNew).
L180588We prove the intermediate
claim HcStep:
((StepState k st) 1) 1 = cNew.
L180590rewrite the current goal using HrpackStep (from left to right).
L180590An
exact proof term for the current goal is
(tuple_2_1_eq rNew cNew).
L180591rewrite the current goal using HgStep (from left to right) at position 1.
L180592rewrite the current goal using HrStep (from left to right) at position 1.
L180593rewrite the current goal using HcStep (from left to right) at position 1.
L180597We prove the intermediate
claim HgxR:
gx ∈ R.
L180599We prove the intermediate
claim HgEq:
g = (State k) 0.
L180600rewrite the current goal using HgEq (from left to right).
L180601An exact proof term for the current goal is (HInv_g_R_A k HkO x HxA).
L180602We prove the intermediate
claim HgxS:
SNo gx.
L180604An
exact proof term for the current goal is
(real_SNo gx HgxR).
L180604We prove the intermediate
claim HrEq:
r = ((State k) 1) 0.
L180608rewrite the current goal using HrEq (from left to right).
L180608An exact proof term for the current goal is (HInv_r_contI k HkO).
L180609We prove the intermediate
claim Hr_fun:
function_on r A I.
L180611We prove the intermediate
claim HrxI:
rx ∈ I.
L180613An exact proof term for the current goal is (Hr_fun x HxA).
L180613We prove the intermediate
claim HrxR:
rx ∈ R.
L180615We prove the intermediate
claim HrxS:
SNo rx.
L180617An
exact proof term for the current goal is
(real_SNo rx HrxR).
L180624An exact proof term for the current goal is (Hu_of_prop r Hr_contI).
L180624We prove the intermediate
claim Hu_contI0:
continuous_map X Tx I0 T0 (u_of r).
L180636We prove the intermediate
claim Hu_fun:
function_on (u_of r) X I0.
L180638We prove the intermediate
claim HuxI0:
ux ∈ I0.
L180640An exact proof term for the current goal is (Hu_fun x HxX).
L180640We prove the intermediate
claim HuxR:
ux ∈ R.
L180642We prove the intermediate
claim HuxS:
SNo ux.
L180644An
exact proof term for the current goal is
(real_SNo ux HuxR).
L180644We prove the intermediate
claim HcEq:
c = ((State k) 1) 1.
L180646We prove the intermediate
claim HcR:
c ∈ R.
L180648rewrite the current goal using HcEq (from left to right).
L180648An
exact proof term for the current goal is
(andEL (((State k) 1) 1 ∈ R) (0 < ((State k) 1) 1) (HInv_cpos k HkO)).
L180652We prove the intermediate
claim HcS:
SNo c.
L180654An
exact proof term for the current goal is
(real_SNo c HcR).
L180660rewrite the current goal using Hcomp (from left to right).
L180664rewrite the current goal using HcorrEq (from left to right).
L180664An
exact proof term for the current goal is
(real_mul_SNo ux HuxR c HcR).
L180669rewrite the current goal using HgNewEval (from left to right).
L180670rewrite the current goal using HcorrEq (from left to right) at position 1.
L180671Set uxc to be the term
mul_SNo ux c.
L180672We prove the intermediate
claim HuxcR:
uxc ∈ R.
L180674An
exact proof term for the current goal is
(real_mul_SNo ux HuxR c HcR).
L180674We prove the intermediate
claim HuxcS:
SNo uxc.
L180676An
exact proof term for the current goal is
(real_SNo uxc HuxcR).
L180679We prove the intermediate
claim HrNumR:
apply_fun rNum x ∈ R.
L180681rewrite the current goal using HrNumEval (from left to right).
L180684rewrite the current goal using HrNewEq (from left to right).
L180685rewrite the current goal using HrNumEval (from left to right) at position 1.
L180689rewrite the current goal using HnumDef (from right to left) at position 1.
L180690We prove the intermediate
claim HnumR:
num ∈ R.
L180692We prove the intermediate
claim HnumS:
SNo num.
L180694An
exact proof term for the current goal is
(real_SNo num HnumR).
L180694We prove the intermediate
claim HdenS:
SNo den.
L180696An
exact proof term for the current goal is
(real_SNo den HdenR).
L180696We prove the intermediate
claim HdivR:
div_SNo num den ∈ R.
L180698An
exact proof term for the current goal is
(real_div_SNo num HnumR den HdenR).
L180698We prove the intermediate
claim HdivS:
SNo (div_SNo num den).
L180700An
exact proof term for the current goal is
(real_SNo (div_SNo num den) HdivR).
L180700We prove the intermediate
claim HcNewDef:
cNew = mul_SNo c den.
L180703rewrite the current goal using HcNewDef (from left to right).
L180707An
exact proof term for the current goal is
(mul_SNo_assoc (div_SNo num den) c den HdivS HcS HdenS).
L180707rewrite the current goal using HmulAssoc (from left to right).
L180711rewrite the current goal using HmulSwap (from left to right).
L180712We prove the intermediate
claim Hdenne0:
den ≠ 0.
L180714An exact proof term for the current goal is H23ne0.
L180714We prove the intermediate
claim Hcancel:
mul_SNo (div_SNo num den) den = num.
L180716An
exact proof term for the current goal is
(mul_div_SNo_invL num den HnumS HdenS Hdenne0).
L180716rewrite the current goal using Hcancel (from left to right).
L180719rewrite the current goal using HnumEq (from left to right).
L180720We prove the intermediate
claim HuxcDef:
uxc = mul_SNo ux c.
L180722rewrite the current goal using HuxcDef (from left to right) at position 1.